Require Import ZArith.
Open Scope Z_scope.

Notation int := nat.



Inductive  value :Set :=
  | Int: Z -> value
  | Bool : bool -> value
  | Tyhp : heap -> value
with heap:Set := 
  | heapemp :heap
  | heapcon : heap->Z->value->heap.
Fixpoint sel (hp : heap) (a : Z) {struct hp} : value :=
  match hp with
    | heapemp => Int 0
    | heapcon hp' a' v => if (Zeq_bool a a') then v else sel hp' a
  end.

Definition upd (hp : heap) (a : Z) (v : value) : heap :=
  heapcon hp a v.
